COMMENT ⊗   VALID 00006 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.if false then begin "notes"
C00003 00003	.s(COMPUT,COMPUTABILITY)
C00005 00004	.ss(cbneval,A Call-by-name LISP interpreter.)
C00016 00005	.ss(noncomput,Non-computability.)
C00029 00006	.ss(lamb,Lambda calculus)
C00052 ENDMK
C⊗;
.if false then begin "notes"
reval.lsp[e80,jmc] 10-sep-80	reval and friends with comments

Recfun theory  LIT...
Connection with lambda calculus?

.end "notes"
.s(COMPUT,COMPUTABILITY)

	The theoretical topics discussed in this chapter are not required
for practical LISP programming.  Neither are they required for proving
correctness of programs - except where they touch on the theory itself.
However, they are interesting, because they concern the fundamental
limitations on what can be done with computers and the connection of LISP
with computational formalisms that have been studied in mathematical logic
since before computers were available.  Moreover, the programming
constructions required for computability theory are particularly easy and
concrete in LISP, and this makes parts of the theory more accessible
than if other computation formalisms are used.

	The mathematical theory of computable functions is thoroughly
treated in (Kleene 1952) and (Davis 1958).  This theory is not concerned
with proving facts about particular programs but rather with the
existence of programs for solving various classes of problems.
Once a problem has been shown to be algorithmically solvable, the
theory of computable functions has little more to say.
.skip
.ss(cbneval,A Call-by-name LISP interpreter.)

	Except for speed and memory size all present day stored program
computers are equivalent in what computations they can do in that any
such computer can be programmed to simulate any other.

	This is well understood intuitively, and the first mathematical
theorem of this kind was proved by A.M. Turing (1936), who defined a
primitive kind of computer now called a Turing machine, and showed how to
make a universal machine that could do any computation done by any Turing
machine when given a description of the machine to be simulated and the
initial tape of the computation to be imitated.
There is no formal definition of ⊗computable apart from computable by
Turing machine or a similar definition based on some other computing
formalism.  Therefore, the best that can be done is to prove different
formalisms equivalent.  (McCarthy 1960) shows how to write a LISP program
for simulating any particular Turing machine which shows that any
Turing computable function is LISP computable.  The converse is an
exercise in Turing machine programming.

	In LISP the function ⊗eval, defined in Chapter_{SECTION READIN}
({eqn evall!!}) is a universal LISP function in the
sense that any computation done by any LISP function can be done by
⊗eval applied to suitable arguments.

	The way ⊗eval handles arguments corresponds to the call-by-value
method of parameter passing in ALGOL and similar languages.  There is also
a form of ⊗eval that corresponds to call-by-name.
The practical difference between call-by-value and call-by-name is that
sometimes a function doesn't need all its arguments, because the values
of some arguments may make the evaluation of others unnecessary.  A trivial
example is that if ⊗x is 0, then the value of the product ⊗xy can be
determined without evaluating ⊗y.  Other examples involve conditional
expressions.  In call-by-value, a subfunction is given the values of
its arguments, while in call-by-name, it is given the location of program
for computing them and can decide which it wants to compute.  If this
were all there is to say, call-by-name would clearly be superior.
However, in straightforward call-by-name, it can happen that an
argument that is used in two different places is computed twice, and
there are other problems.  Most LISPs use call-by-value, mainly
for the historical reason that call-by-name was invented later in
connection with Algol.

	Here is a call-by-name ⊗eval called ⊗neval: 
.begin nofill turnon "∂"
.n←8

∂(n)  ⊗⊗	neval[e, a] ← ⊗
∂(n)  ⊗⊗	qif qat e qthen⊗
∂(n)  ⊗⊗		[qif e = qT  qthen qT⊗
∂(n)  ⊗⊗		qelse qif e = qNIL qthen qNIL⊗
∂(n)  ⊗⊗		qelse qif numberp e qthen e⊗
∂(n)  ⊗⊗		qelse neval[qad assoc[e, a], qdd assoc[e, a]]]⊗
∂(n)  ⊗⊗	qelse qif qat qa e qthen⊗
∂(n)  ⊗⊗		[qif qa e = $CAR qthen qa neval[qad e, a]⊗
∂(n)  ⊗⊗		qelse qif qa e = $CDR qthen qd neval[qad e, a]⊗
!fcnneval& ∂(n)  ⊗⊗		qelse qif qa e = $CONS qthen neval[qad e, a] . neval[qadd e, a]⊗
∂(n)  ⊗⊗		qelse qif qa e = $ATOM qthen qat neval[qad e, a]⊗
∂(n)  ⊗⊗		qelse qif qa e = $EQ qthen neval[qad e, a] = neval[qadd e, a]⊗
∂(n)  ⊗⊗		qelse qif qa e = $QUOTE qthen qad e⊗
∂(n)  ⊗⊗		qelse qif qa e = $COND qthen nevcon[qd e, a]⊗
∂(n)  ⊗⊗		qelse qif qa e = $LIST qthen mapcar[qd e, λx: neval[x, a]]⊗
∂(n)  ⊗⊗		qelse neval[qd assoc[qa e, a] . qd e, a]]⊗
∂(n)  ⊗⊗	qelse qif qaa e = $LAMBDA qthen neval[qadda e, nprup[qada e, qd e,  a]]⊗
∂(n)  ⊗⊗	qelse qif qaa e = $LABEL qthen neval[qadda e . qd e, [qada e . qa e] . a]⊗, 
.end

where the auxiliary function ⊗nevcon is given by

!fcnnevcond& ⊗⊗⊗nevcon[u, a] ← qif neval[qaa u, a] qthen neval[qada u, a] qelse nevcon[qd u, a]⊗.

and ⊗nprup is

!fcnnprup& ⊗⊗⊗nprup[u, v,a] ← qif qn u qthen a qelse [qa u . [qa v . a]] . nprup[qd u, qd v,a]⊗.

	⊗eval and ⊗neval differ only in two terms.
⊗eval evaluates a variable by looking it up on the association list whereas
⊗neval looks it up on the association list and evaluates the result
in the context in which it was put on the association list.
Thus constants on the ⊗neval association list must be quoted.
Correspondingly, when a λ-expression is encountered, ⊗eval forms a new
association list by pairing the values of the arguments with the variables
bound by the λ and putting the new pairs in front of the old association list, 
whereas ⊗neval pairs the arguments themselves with the
variables and puts them on the front of the association list.  The function
⊗neval also saves the current association list with each variable on the 
association list, so that the variables can be evaluated in the correct context.
In most cases they give the same result with the same work, but ⊗neval 
gives a result for some functions of several arguments for
which ⊗eval loops.  An example is
obtained by evaluating ⊗⊗F[1, 0]⊗ where ⊗F is defined by

⊗⊗⊗F[m, n] ← qif m=0 qthen 0 qelse F[m-1, F[m, n]]⊗.

⊗eval always loops, because in order to evaluate ⊗⊗F[m, n]⊗, it must
when ⊗m isn't 0, it must evaluate both arguments of ⊗⊗F[m-1, F[m, n]]⊗,
and one of them is ⊗⊗F[m, n]⊗ again.  When ⊗neval evaluates ⊗⊗F[1, 0]⊗,
it finds itself evaluating ⊗⊗F[1-1, F[1, 0]]⊗, which expands to
⊗⊗qif 0=0 qthen 0 qelse F[0-1, F[1,0]]⊗, and this is evaluated without
further recursion.

	Vuillemin [1973] showed that if a function is ⊗strict, i.e. never
has a defined value unless each argument has a defined value, then
call-by-name and call-by-value always give the same result.
When the functions have free variables as parameters, the situation
is more complicated.
.SKIP 
.cb Exercises

1. Write ⊗neval and the necessary auxiliary functions in list
form, and try them out on some examples.

2. Suppose a variable has several occurrences in a λ-expression, and
this variable is bound to a complicated expression by ⊗neval.  Each
time the variable is reached by ⊗neval, the complicated expression
is re-evaluated.  Make a version of ⊗neval that uses ⊗rplacd to
replace the expression by quoting the result of evaluating it
the first time the expression is evaluated, so that subsequent
evaluations of the variable find a quoted constant.

3. If you know about Turing machines, write a LISP function to
simulate an arbitrary Turing machine given a description of the
machine in some convenient notation.

4. Write a LISP function that will translate a Turing machine
description into a LISP function that will do the same computation.

5. If you really like Turing machines, write a description of
a Turing machine that will interpret LISP internal notation.
.ss(noncomput,Non-computability.)

	Some of the most surprising results in mathematics are proofs
that something cannot be done, especially when many people have spent
years trying.  While it is supposed that mathematicians are merely
elevating their failure to solve a problem into a general principle,
completely convincing impossibility proofs often exist.
The first such result of was the discovery by the Pythagoreans
that the square root of 2 is irrational, i.e. that no-one
can find a square with integer sides and an integer diagonal.  The
nineteenth century brought the unsolvability of the three ancient
straight-edge-and-compass construction problems - trisecting angles,
duplicating the cube, and squaring the circle.

	Perhaps the most spectacular and philosophically significant
results of this kind were obtained in the 1930s when it was shown that
no general methods exist for deciding certain well-known problems.
LISP provides a convenient way of showing the existence of a problem
undecidable by LISP computation - whether a LISP computation terminates
or goes on indefinitely.

	Some LISP calculations run on indefinitely.  The most trivial
case occurs if we make the recursive definition

!fcnloop&forever ⊗⊗⊗loop x ← loop x		⊗

and attempt to compute ⊗⊗loop[x]⊗ for any ⊗x whatsoever.  Don't
dismiss this example just because no-one would
write such an obviously useless
function definition.  It is the
"zero" of a certain class function definitions, and, 
as the Romans experienced but never learned, leaving zero out of the number
system is a mistake.

	Nevertheless, in most programming, non-terminating calculations are
the results of errors in defining functions.  Therefore, it would be
useful to be able to tell whether a function definition gives a
result for all arguments.  In fact, it would be useful to be able to tell
whether a function will terminate for a single argument.  Let us make
this goal more precise.

	Suppose that ⊗f is a LISP function and ⊗a is an S-expression, 
and we would like to know whether the computation of ⊗f[a] terminates.
Suppose ⊗f is represented by the S-expression ⊗f* in internal
notation.  Then the S-expression $$(⊗f* (QUOTE ⊗⊗a⊗))$
represents ⊗f[a].  Define the function ⊗term by giving
⊗term[e] the value qtrue if ⊗e is an S-expression of the
form $$(⊗f* (QUOTE ⊗⊗a⊗))$ for which ⊗f[a] terminates and qfalse otherwise.
⊗term is a perfectly well-defined function, because we have just defined it,
but we can ask whether it is a LISP function.
Can it be constructed
from ⊗car, ⊗cdr, ⊗cons, ⊗atom,  and ⊗eq using ⊗λ, ⊗label, and
conditional expressions?  Well, it can't, as we shall shortly prove, 
and this means that it is not ⊗computable whether a LISP calculation
terminates, since if ⊗term were computable by any computer or in any
recognized sense, it could be represented as a LISP function.  Here is the
proof:

	Consider the function ⊗terma defined from ⊗term by

!fcnterma& ⊗⊗⊗terma u ← qif term list[u, list[$QUOTE, u]] qthen loop u qelse qtrue⊗, 

and suppose that ⊗f is a LISP function and that ⊗f* is its
S-expression representation.

	What is ⊗terma ⊗f*?  Like ⊗term ⊗f*, it
tells us whether the computation of ⊗f[f*] 
terminates, but it tells us this by going into a loop if ⊗f[f*] 
terminates and giving qtrue otherwise.  Now if ⊗term were
a LISP function, then ⊗terma would also be a LISP function.  Indeed if
⊗term were represented by the S-expression ⊗term*, then
⊗terma would be represented by the S-expression

!fcntermastar& ⊗⊗⊗terma*⊗ = $$(LAMBDA (U) (COND ((⊗term* (LIST U (LIST (QUOTE QUOTE) U))) (LOOP U)) (T T)))$.

Now consider ⊗terma[terma*].   According to the definition of ⊗terma, 
this will tell us whether ⊗terma[terma*] is defined, i.e. it tells
about itself.  However, it gives this answer in a contradictory way; namely
⊗terma[terma*] looping tells us that ⊗terma[terma*] terminates, 
and ⊗terma[terma*] being qtrue tells us that ⊗terma[terma*] 
doesn't terminate.  Our assumption that ⊗term was a LISP function is
thereby refuted, and there is no general procedure for telling whether
a LISP calculation terminates.  It is not logically excluded that there
might be some more powerful means of effectively determining whether LISP
computations terminate, because the notion of "effectively determining"
is not definite.  However, all the formal notions of "effectively determining"
that have been proposed, including LISP computability, turn out to be
mutually equivalent.

	The above proof is the same in principle as Turing's proof that
there is no Turing machine that tells whether Turing machine computations
terminate.  However, the technical details are simpler, because LISP
is more facile than the Turing machine formalism at such constructions
as the one that tells how to construct ⊗terma from ⊗term.  Other problems
are proved unsolvable by showing that a method for solving them would
lead to a method for determining whether a computation terminates.
(Davis 1958) is a good reference.

	The above result does not exclude LISP functions that tell whether
some LISP calculations terminate.  It just excludes methods that work
on all LISP calculations.  This result can be strengthened.

	Suppose
a LISP function ⊗term sometimes says a calculation terminates, 
sometimes says a calculation doesn't terminate,
and sometimes runs on indefinitely.
Further suppose that when ⊗term gives an
answer it is always right.  We can further assume that ⊗term[e]_=_T 
whenever the calculation represented by ⊗e terminates.
This can be assured by mixing the computation of ⊗term[e] 
with a computation of ⊗⊗eval[e,_qNIL]⊗ and doing the computations
alternately.  If the ⊗⊗eval[e,_qNIL]⊗ computation ever terminates, 
then the new function asserts termination.

	Given such a ⊗term, we can always find a calculation ⊗e that
does not terminate but ⊗term doesn't say so.  The construction is just like that
used in the previous proof.  We construct

!fcnta&  ⊗⊗⊗terma u ← qif term list[u, list[$QUOTE, u]] qthen loop u qelse qtrue⊗, 

and then we consider ⊗terma[terma*].  If this had the value qtrue, 
then it wouldn't terminate so therefore it doesn't terminate but is
not one of those expressions which ⊗term decides.  Thus for any
partial decider we can find a LISP calculation which doesn't terminate
but which the decider doesn't decide.
This can in turn be used to get a slightly better decider, namely

!fcntq1& ⊗⊗⊗term%41%*[e] ← qif e = terma* qthen $DOESN'T-TERMINATE  qelse term[e]⊗.

.turnon "↓"
Of course, ⊗⊗term⊗%41%* isn't much better than ⊗term, since it can decide
only one more computation, but we can form ⊗⊗term⊗%42%* by applying the same
process, and so forth.  In fact, we can even form ⊗⊗term⊗%8↓w%* which
decides all the cases decided by any ⊗⊗term⊗%4n%*.  This can be further
improved by the same process, etc.  How far can we go?  The answer is
technical; namely, the improvement process can be carried out any
recursive ordinal number of times.

	Unfortunately, this kind of improvement is superficial, 
since none of the new computations proved not to terminate are likely
to be of practical interest.
.SKIP
.cb Exercises

1. Write a function that gives ⊗⊗term⊗%4n+1%* in terms of ⊗⊗term⊗%4n%*.

2. Write a function that gives ⊗⊗term⊗%8↓w%* in terms of ⊗term. 

3.  A LISP predicate  ⊗term is called a termination  tester if
for any  S-expression ⊗e, ⊗term[e] = $T if  and only if the LISP
evaluation of  ⊗e  terminates; otherwise  ⊗term[e] = $F  or  is
undefined.   Thus we must have  ⊗term[$(CAR (QUOTE (A)))] = $T, and
%2term[%1((LABEL FOO (LAMBDA (X) (FOO X))) NIL)] may have the value $F 
or  may   be  undefined.      Let  ⊗term*   be  the   S-expression
representation of ⊗term. 

	Write a LISP function ⊗bad such that for any termination
tester ⊗term, ⊗bad[term*] is defined, but ⊗term[bad[term*]] 
is undefined.  Show that your ⊗bad works.

Hint: A two line answer is possible using ⊗subst and the function
⊗⊗quine[x] = subst[x,$$X,(X (QUOTE X))$]⊗. 
.turnoff
.ss(lamb,Lambda calculus)

	The lambda notation used in LISP was taken from the lambda
calculus developed by Alonzo Church in the late 1920s
and described in his 1940 book, %2The Calculi
of Lambda Conversion%1.  This section covers some aspects of the
lambda calculus that go beyond what is used in LISP.

	Each LISP expression either evaluates to some object 
(like %2qa x%1)
or it
represents a function (like %2λx.[qa x_._y]%1).
[In the terminology of logic, it has a definite
type, but the word "type" is often used differently in computer science
where numbers and list structure are considered of different types.
Logicians use the word "sort" for the computer scientist's "type"].
The lambda calculus
doesn't make this distinction, and any expression can be taken as
a function.

	Lambda calculus is much simpler than LISP in its basic structure,
and its well-formed formulas (abbreviated wffs) are constructed as follows:

.item←0
	#. A variable is a wff.

	#. If ⊗f and ⊗e are wffs, then so is ⊗f(e). 

	#. If ⊗v is a variable and ⊗e is a wff,
then ⊗(λv.e) is a wff.
.<<should we introduce a list form of λ-expression here?>>

	#. An expression is a wff only if its being a wff follows
from the above rules.

	Here are some examples.

.item←0
	#. ⊗x and ⊗y are wffs by rule 1.

	#. ⊗x(x), ⊗x(y), ⊗y(x) and ⊗(x(y))(x) are wffs.  The same
symbol can and often does appear in both function and argument
positions.

	#. ⊗(λx.(λy.x)), ⊗(λx.(λy.y)) and ⊗(λf.(λx.f(x(x)))(λx.f(x(x)))) 
are all wffs that will be important in subsequent developments.

	The occurrences of variables in a λ-expression may be divided into
free and bound occurrences.  Any occurrence of ⊗x within an
expression ⊗(λx.exp) is a bound occurrence.  The expression represented
by ⊗exp is called the scope of this occurrence of ⊗λx.  Other occurrences
are called free, and sometimes the variables themselves are called free
or bound.  This is a misnomer, because a given variable may have both
free and bound occurrences in a particular wff.
An occurrence of a variable ⊗x is called bound by
⊗λx in ⊗λx.exp if it is free in ⊗exp.  In the last λ-expression in example
3 above, each ⊗λx binds two occurrences of ⊗x. 

	Just as in LISP
or in logic or in definite integrals in calculus, bound variables may
be changed without changing the meaning of the expression provided all
occurrences in the scope of a given variable binder
are changed and no variable that is free in a subexpression
becomes bound.  Thus we may change ⊗(λx.(λy.x)) to ⊗(λu.(λy.u)) without
changing the meaning of the expression.  However, we could not change
the ⊗x in ⊗(λx.(λy.y)) to ⊗y without changing the ⊗y to something
else first, because this would give ⊗(λy.(λy.y)) which replaces the
second occurrence of ⊗x by a variable which is now bound by the
second λ.  This kind of change of variables is called an alphabetic
change and is also referred to as αα-conversion.

	The second kind of conversion is λ-conversion.  It can be
done when a wff consists of a λ-expression applied to another wff.
An example is ⊗(λx.x(y))(u), and the general form is
⊗(λx.e1)(e2).  The conversion consists essentially in replacing
the given expression by the result of substituting ⊗e2 for
⊗x in ⊗e1.  Thus the above-mentioned ⊗(λx.x(y))(u) converts to
⊗u(y).  

	There is a catch.  Suppose we want to convert
⊗(λx.(λy.x(y)))(y(y)).  If we simply subsitute ⊗y(y) for ⊗x in
⊗(λy.x(y)), the free occurrences of ⊗y in ⊗y(y) will become bound
giving ⊗(λy.y(y)(y)), and this isn't allowed, because it would
change the intended meaning of the λ-expression.  When a λ-conversion
will result in the "capture" of a free occurrence of a variable,
it must be preceded by a change of bound variables.  In the above
example, we can replace the bound occurrences of ⊗y before doing
the λ-conversion and get first ⊗(λx.(λu.x(u)))(y(y)) and then
⊗(λu.y(y)(u)).  In thinking about programs to do
λ-conversion, it is usually convenient to regard the preliminary
αα-conversion that may be needed as part of the λ-conversion
rather than as a precondition.

	We write ⊗e1_→_e2 as a way of saying that ⊗e1 converts
to ⊗e2.  We include conversions of subexpressions as λ-conversions.
Here are some examples of λ-conversion.

.begin nofill turnon "∂"
.n←8

	⊗⊗(λx.(λy.x))(a)(b) → (λy.a)(b) → a⊗

	⊗⊗(λx.(λy.y))(a)(b) → (λy.y)(b) → b⊗

	⊗⊗(λx.f(x(x)))(λx.f(x(x))) → f(λx.f(x(x)))(λx.f(x(x))))⊗.
.end

Each of them will be important.

	A wff which is not subject to λ-conversion is said to
be in normal form.  Some λ-expressions can be converted successively
0 or more times and will eventually reach a normal form.  The first
two conversions above are reductions to a normal form.  The third
example is not reduced to normal form, and it is is clear that it can't
be, because the argument of ⊗f on the right is just the whole expression
on the left.  We have

	⊗⊗e → f(e) → f(f(e)) → f(f(f(e))) →⊗ etc.

	Sometimes a wff may be convertible in several ways, because several of
its subexpressions may be applications of a λ-expression to another
expression.  Whether a normal form is reached may depend on the
order in which reductions are done.  However, the Church-Rosser
theorem of 1936 asserts that if a normal form is reached by some
sequence of conversions, it is unique; different conversion paths
cannot give rise to different normal forms.  It can happen, however,
that some paths give a normal form and others don't.

	Church originally proposed the λ-calculus as a way of
formalizing the foundations of mathematics, and the original
version included logical operations and quantifiers.  Unfortunately,
this system proved inconsistent (any formula was provable) and
had to be abandoned.  However, Church was able to show that arithmetic
computations could be encoded as reductions of λ-expressions to
normal form, and it was shown in the 1930s that λ-computations and
Turing machine computations were equally powerful.

	When we compare reduction of λ-expressions to normal form
to LISP computations, it seems surprising that any significant
computing can be done with only λ-conversion.  There are apparently
no lists, no qqa , qqd or ⊗cons, no conditional expressions and
no recursion.  However, as we shall now show all these things can
be done in the λ-calculus.  While Church first showed how to do
computation in λ-calculus, the most straightforward and instructive
course for us is to use constructions due essentially to Dana Scott that
imitate pure LISP.

	First we need a slightly abbreviated notation.
All our functions have had just one argument, but the value of a function
can be another function, and this is enough to imitate functions
of several arguments.  The idea is to regard ⊗f(x,y) as just an
abbreviation of ⊗f(x)(y), i.e. to regard a function of two arguments
as a function of one argument (the first argument) whose value 
is a function of one argument (the second argument).  We then
also regard ⊗(λx_y.e) as an abbreviation of ⊗(λx.(λy.e)).

	We now proceed by identifying certain objects and functions
of LISP as certain λ-expressions.

	We begin with truth values and write

	⊗⊗true = (λx y.x) = (λx.(λy.x))⊗

and 

	⊗⊗false = (λx y.y) = (λx.(λy.x))⊗. 

So far this is quite arbitrary, and the motivation for these
identifications is not apparent.  Now we do conditional
expressions and write

	⊗⊗qif p qthen a qelse b = p(a)(b) = p(a,b)⊗, 

and we already get a return from our investment.  Namely,

	⊗⊗qif true qthen a qelse b = true(a)(b) = (λx y.x)(a,b) → a⊗, 

which is just the property this conditional expression should have.
Likewise

	⊗⊗qif false qthen a qelse b = false(a)(b) = (λx y.y)(a,b) → b⊗.

Using this conditional expression notation,
we can define the propositional connectives as

	⊗⊗p ∧ q = qif p qthen q qelse false = p(q,false)⊗

	⊗⊗p ∨ q = qif p qthen true qelse q = p(true,q)⊗

	⊗⊗¬p = qif p qthen false qelse true = p(false,true)⊗,

and all the usual truth table reductions immediately follow by reducing
the λ-expressions to normal form.  For example

	⊗⊗true ∧ false = true(false,false) = (λx y.x)(false,false) → false⊗.

It is important to notice that this only works if the
propositional argument ⊗p of "⊗⊗qif_p_qthen_a_qelse_b⊗" converts to ⊗true or
⊗false.  In LISP anything but ⊗false behaves like ⊗true, but there is
no way to make this happen in λ-calculus.

	Next we need ⊗car, ⊗cdr and ⊗cons.  We begin with versions that
meet part of our requirements and will use them to construct the final
versions.
We write

	⊗⊗cons1 = (λ x y z.z(x,y))⊗

	⊗⊗car1 = (λx.x(true))⊗

	⊗⊗cdr1 = (λx.x(false))⊗,

which seem mysterious, but it is comforting to observe that

.begin nofill turnon "∂"
.n←8

∂(n)  ⊗⊗car1(cons1(e1,e2)) ∂(n+16)= (λx.x(true))(cons1(e1,e2))⊗

∂(n+16)  ⊗⊗→ cons1(e1,e2)(true)⊗

∂(n+16)  ⊗⊗= (λx y z.z(x,y))(e1,e2,true)⊗

∂(n+16)  ⊗⊗→ true(e1,e2)⊗

∂(n+16)  ⊗⊗→ e1⊗
.end

	Likewise

	⊗⊗cdr1(cons1(e1,e2)) →→ e2⊗

where →→ refers to eventual reduction rather than a single step.
Thus ⊗cons1 has one main property of a pairing operation in that
⊗car1 and ⊗cdr1 enable us to get the operands back.  However, we
lack atoms and a way of identifying them.  We get them by defining
an atom qnil and new λ-expressions ⊗cons, ⊗car and ⊗cdr. 

	Our example system will have a single atom qnil, and we define

	⊗⊗qnil = cons1(true,true)⊗

Now we can define a ⊗cons that produces imitation S-expressions that
can be distinguished from our imitation atom qnil.

	⊗⊗cons = (λx y.cons1(false,(cons1(x,y)))⊗

	⊗⊗car = (λx.car1(cdr1(x)))⊗

	⊗⊗cdr = (λx.cdr1(cdr1(x)))⊗

	⊗⊗null = (λx.car1(x))⊗.

The idea is that the atom qnil has its ⊗car1 part ⊗true, while every
expression produced by ⊗cons has its ⊗car1 part ⊗false.  Therefore,
we use the ⊗car1 part in conditional expressions as a test for ⊗null. 

	Finally, to get recursion, we write

	⊗⊗recur = (λf.(λx.f(x(x)))(λx.f(x(x))))⊗, 

which is Church's famous Y combinator.
The property that makes it useful for defining recursion,
as mentioned above, is that

	⊗⊗recur(f) → f(recur(f)) → f(f(recur(f))) → ⊗etc.

Notice that ⊗recur is not in normal form, since it contains an application
of a λ-expression inside it.  Moreover, the above "fixed point" property
shows that it has no normal form.

	Now we can do pure LISP.  We can write

	⊗⊗append = recur(λf.(λu v.qif null(u) qthen v qelse cons(car(u),
f(cdr(u),v))))⊗

and

	⊗⊗equal = recur(λf.(λx y.(null(x) ∧ null(y) ∨ (¬null(x) ∧ ¬null(y))
∧ (f(car(x),car(y)) ∧ f(cdr(x),cdr(y))))))⊗

	Using the above abbreviations we can show such facts as

	⊗⊗append(qnil,qnil) → qnil⊗

	⊗⊗append(cons(qnil,qnil),qnil) → cons(qnil,qnil)⊗

	⊗⊗equal(qnil,qnil) → true⊗

	⊗⊗equal(cons(qnil,qnil),qnil) → false⊗.

The expressions on the right are all abbreviations of normal forms.

	There are two catches.  First, while the Church-Rosser theorem
assures us that if we get an answer it will be unique, it doesn't assure
us that all sequences of reduction get answers, and some don't.  Suppose
we are computing ⊗append(qnil,qnil).  We make the abbreviation

	⊗⊗app1 = qif null(u) qthen v qelse cons(car(u),f(cdr(u),v))⊗

and have

.begin nofill turnon "∂"
.n←8

∂(n)  ⊗⊗append(qnil,qnil) ∂(n+15)= recur(λf u v.app1)(qnil,qnil)⊗

∂(n+15)  ⊗⊗→ (λf u v.app1)(recur(λf u v.app1))(qnil,qnil)⊗. 
.end

At this point two conversions are possible.  We could convert the
new ⊗recur(λf u v.app1)
or we can convert the application of ⊗⊗λf_u_v.app1⊗ to its arguments
and get

	⊗⊗→ qif null(qnil) qthen qnil qelse cons(car(qnil),recur(λf u v.app1)(cdr(qnil),qnil))⊗.

The former could go on indefinitely, while the
latter is what imitates the usual LISP computation and promptly
leads to a normal form.  The general rule is to do first the
outermost possible reduction.  It can be shown that this rule leads to
a normal form whenever a normal form exists.  It corresponds to a call-by-name
evaluation rule.

	The preceding shows how to translate any pure LISP function as
a wff of λ-calculus.  If we also encode its arguments and form
the wff consisting of the application of the function to its
arguments and then normalize ⊗e, the process will terminate
provided the LISP computation taken in the call-by-name sense
terminates, and the resulting normal form will be an encoding
of the result of the LISP computation.

	The second catch is that the λ-calculus provides no way of
making or proving general statements.  While every individual case
of ⊗⊗append(append(u,v),w)⊗ will reduce to the same normal form
as ⊗⊗append(u,append(v,w))⊗, the λ-calculus provides no way of
stating or proving it within the formalism.  Of course, it isn't hard
to show by informal reasoning ⊗about the λ-calculus.  Church's original
1920s inconsistent formalism did provide for general statements.

	Here are some remarks.
.item←0

	#. Reducing to normal form even simple imitation LISP expressions
like ⊗append(cons(qnil,qnil),cons(qnil,qnil)), i.e. imitating the computation of
⊗⊗(qnil)*(qnil) = (qnil qnil)⊗, is a long computation best done by a
λ-calculus reduction program written in LISP.

	#. Further definitions could give an improved language for
LISP in λ-calculus.  One way to get more atoms is to
regard a certain class of composite expressions formed with
⊗cons1 as atoms just as we did with ⊗qnil. 

	#. The LISP in λ-calculus formalism works only if all expressions
that occur in the computation are constructed in the manner provided for.
Including general λ-expressions even as list elements can cause strange
results when an attempt is made to normalize them.

	#. While encoding LISP in λ-calculus shows that λ-calculus
is universal in its computing capabilities, this doesn't seem to
be a good way of taking advantage of the ability of the λ-calculus
to express functions of higher type.